es:ES, T:Type, c:T, i, x:Id, e:E.
@i x initially c:T  (loc(e) = i)  {@i(x:T) c ((x when first-event{i:l}(es;e)) = c)} 

latex

Definitions	ES, Type, x:A. B(x), E, @i x initially v:T, P  Q, Id, {T}, A c B, x:A  B(x), s = t, @i(x:T), first-event{i:l}(es;e), e@i. P(e), P  Q, P & Q, P  Q, x:AB(x), isrcv(e), s ~ t, t  T, SQType(T), if b then t else f fi , e loc e' , (e <loc e'), t.1, Atom$n, b
Lemmas	es-le-loc, Id sq, es-isrcv-loc, first-event-property, init-p-implies